VERS5 
NIL 
((IRREFLEXIVITY_OF_ORDER NATNUM#7) (TRANSITIVITY_OF_ORDER NATNUM#8) (ZEROLEAST1 NATNUM#9) (SUCCESSOR1 NATNUM#11) (SUCCESSOR2 NATNUM#12) (SUCCESSORLESS NATNUM#13) (SUCCESSOREQ NATNUM#14) (ZEROLEAST2 NATNUM#15) (ZEROLEAST3 NATNUM#16) (ZERO_NOT_SUCCESSOR NATNUM#17) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (COMMUTADD NATNUM#29) (TIMSUCC NATNUM#33) (LTIMESCAN NATNUM#34) (RTIMESCAN NATNUM#35) (COMMUTMULT NATNUM#36) (LTIMESTOZERO NATNUM#37) (RTIMESTOZERO NATNUM#38) (LDISTRIB NATNUM#39) (RDISTRIB NATNUM#40) (PROOF_BY_INDUCTION INDUCTION#1) (INDUCTIVE_DEFINITION INDUCTION#5) (PROOF_BY_DOUBLEINDUCTION INDUCTION#6) (HIGH_ORDER_NATNUM_DEFINITION INDUCTION#10) (INFINITE_DESCENT INDUCTION#11) (UNIVDEF SET#4) (INTERDEF SET#6) (UNIONDEF SET#8) (INCLUSIONDEF SET#10) (INVERSEDEF SET#12) (INVERSEPROP SET#13) (INVERSEPROP1 SET#14) (EPSILONDEF SET#16) (TRANSDEF SET#18) (SEGMDEF SET#20) (TAILDEF SET#22) (INDUCTIVE_SET_DEFINITION INDUCTION#15) (TRANSITIVE_INDUCTION INDUCTION#16) (COURSE_OF_VALUES_DEFINITION INDUCTION#17) (MAXDEF MINMAX#5) (MINDEF MINMAX#6) (MINPROP MINMAX#9) (MINPROP1 MINMAX#10) (MINPROP2 MINMAX#11) (UNBOUNDEF UNBOUND#2) (SPLIT_UNBOUND UNBOUND#4) (BOUNDSORT UNBOUND#6) (BOUNDFACT UNBOUND#7) (SUCCFACTS NATNUM#11 NATNUM#12 NATNUM#13 NATNUM#14 NATNUM#15 NATNUM#16 NATNUM#17) (TIMESFACTS NATNUM#30 NATNUM#32 NATNUM#33 NATNUM#34 NATNUM#35 NATNUM#36 NATNUM#37 NATNUM#38 NATNUM#39 NATNUM#40) (PLUSFACTS NATNUM#21 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 NATNUM#29 NATNUM#39 NATNUM#40) (SIMPINFO NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8 UNBOUND#2 UNBOUND#3 UNBOUND#6)) (NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . NATNUM#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 5 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 6 .)(NIL . (DECL (F FUNCT) (TYPE: (TY& . GROUND→GROUND))) . ((FUNCT . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#1 . NIL . VARIABLE .)) (F . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . SET . NIL . 1 .)(NIL . (DECL (REL) (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|))) . ((REL . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . SET . NIL . 2 .)(NIL . (DECL MAX (TYPE: (TY& . |((GROUND⊗GROUND)∨(GROUND→TRUTHVAL))→GROUND|)) (SYNTYPE: CONSTANT)) . ((MAX . (|((GROUND⊗GROUND)∨(GROUND→TRUTHVAL))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MINMAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . MINMAX . NIL . 1 .)(NIL . (DECL MIN (TYPE: (TY& . |((GROUND⊗GROUND)∨(GROUND→TRUTHVAL))→GROUND|)) (SYNTYPE: CONSTANT)) . ((MIN . (|((GROUND⊗GROUND)∨(GROUND→TRUTHVAL))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . MINMAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . MINMAX . NIL . 2 .)(|∀N.¬N<N| . (AXIOM (TM& . |∀N.¬N<N|)) . (LESSP M N K J I) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (LESSP M N K J I) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (LESSP M N K J I) . NIL . (NATNUM#9) . NIL . NATNUM . NIL . 9 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (ADD1 M N K J I) . NIL . (NATNUM#10) . NIL . NATNUM . NIL . 10 .)(|∀N.N<N'| . (AXIOM (TM& . |∀N.N<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#11) . NIL . NATNUM . NIL . 11 .)(|∀N M.¬N<M⊃M<N'| . (AXIOM (TM& . |∀N M.¬N<M⊃M<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#12) . NIL . NATNUM . NIL . 12 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (ADD1 M N K J I) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (LESSP M N K J I) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.0<N'| . (AXIOM (TM& . |∀N.0<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (ADD1 M N K J I) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(NIL . (DECL PRED (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#18 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 18 .)(|∀N.PRED(N')=N| . (DEFAX PRED (TM& . |∀N.PRED(N')=N|)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#19 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (ADD1 M N K J I SET C B A) . NIL . (INDUCTION#1) . NIL . INDUCTION . NIL . 1 .)(NIL . (DECL NPARS (TYPE: (TY& . GROUND*))) . ((NPARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 2 .)(NIL . (DECL NDF (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((NDF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 3 .)(NIL . (DECL ZCASE (TYPE: (TY& . |(GROUND*)→GROUND|))) . ((ZCASE . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#4 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 4 .)(NIL . (DECL UNIV (TYPE: (TY& . @SET))) . ((UNIV . (@SET . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#3 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SET . NIL . 3 .)(|∀N M.NATNUM(MIN(N,M))| . (AXIOM (TM& . |∀N M.NATNUM(MIN(N,M))|)) . (M N K J I MIN) . NIL . (MINMAX#3) . NIL . MINMAX . NIL . 3 .)(|∀N M.NATNUM(MAX(N,M))| . (AXIOM (TM& . |∀N M.NATNUM(MAX(N,M))|)) . (M N K J I MAX) . NIL . (MINMAX#4) . NIL . MINMAX . NIL . 4 .)(|∀N M K.K<MAX(N,M)≡K<N∨K<M| . (AXIOM (TM& . |∀N M K.K<MAX(N,M)≡K<N∨K<M|)) . (LESSP M N K J I MAX) . NIL . (MINMAX#5) . NIL . MINMAX . NIL . 5 .)(|∀N M K.K<MIN(N,M)≡K<N∧K<M| . (AXIOM (TM& . |∀N M K.K<MIN(N,M)≡K<N∧K<M|)) . (LESSP M N K J I MIN) . NIL . (MINMAX#6) . NIL . MINMAX . NIL . 6 .)(|∀A.NATNUM(MAX(A))| . (AXIOM (TM& . |∀A.NATNUM(MAX(A))|)) . (SET C B A MAX) . NIL . (MINMAX#7) . NIL . MINMAX . NIL . 7 .)(|∀A.NATNUM(MIN(A))| . (AXIOM (TM& . |∀A.NATNUM(MIN(A))|)) . (SET C B A MIN) . NIL . (MINMAX#8) . NIL . MINMAX . NIL . 8 .)(|∀A.(∃N.A(N))⊃A(MIN(A))| . (AXIOM (TM& . |∀A.(∃N.A(N))⊃A(MIN(A))|)) . (M N K J I SET C B A MIN) . NIL . (MINMAX#9) . NIL . MINMAX . NIL . 9 .)(|∀A.(∀N.N<MIN(A)⊃¬A(N))| . (AXIOM (TM& . |∀A.(∀N.N<MIN(A)⊃¬A(N))|)) . (LESSP M N K J I SET C B A MIN) . NIL . (MINMAX#10) . NIL . MINMAX . NIL . 10 .)(NIL . (DECL UNBOUND (TYPE: (TY& . |(@SET)→TRUTHVAL|))) . ((UNBOUND . (|(@SET)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . UNBOUND#1 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . UNBOUND . NIL . 1 .)(|∀N.NATNUM(PRED(N))| . (AXIOM (TM& . |∀N.NATNUM(PRED(N))|)) . (ADD1 M N K J I PRED) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#21 . NIL . DEFINED .)) ADD1 M N K J I) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))| . (AXIOM (TM& . |∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))|)) . (ADD1 M N K J I NPARS NDF ZCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .)) (NDEF . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .))) . NIL . (INDUCTION#5) . NIL . INDUCTION . NIL . 5 .)(|∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))| . (AXIOM (TM& . |∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))|)) . (ADD1 M N K J I (A2 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#6 . NIL . VARIABLE .))) . NIL . (INDUCTION#6) . NIL . INDUCTION . NIL . 6 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 7 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#29) . NIL . NATNUM . NIL . 29 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#30 . NIL . DEFINED .)) ADD1 PLUS M N K J I) . NIL . (NATNUM#30) . NIL . NATNUM . NIL . 30 .)(NIL . (DECL INDFN (TYPE: (TY& . |(GROUND⊗(@ARB))→(@ARB)|))) . ((INDFN . (|(GROUND⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#8 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 8 .)(NIL . (DECL (DEF_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((DEF_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#9 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 9 .)(|∀N M.NATNUM(M*N)| . (AXIOM (TM& . |∀N M.NATNUM(M*N)|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#31) . NIL . NATNUM . NIL . 31 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#32) . NIL . NATNUM . NIL . 32 .)(|∀N K.N*K'=N*K+N| . (AXIOM (TM& . |∀N K.N*K'=N*K+N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#33) . NIL . NATNUM . NIL . 33 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#34) . NIL . NATNUM . NIL . 34 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#35) . NIL . NATNUM . NIL . 35 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#36) . NIL . NATNUM . NIL . 36 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#37) . NIL . NATNUM . NIL . 37 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#38) . NIL . NATNUM . NIL . 38 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#39) . NIL . NATNUM . NIL . 39 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#40) . NIL . NATNUM . NIL . 40 .)(|∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))| . (AXIOM (TM& . |∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))|)) . (ADD1 M N K J I ARB2 ARB1 ARB INDFN DEF_FUN) . NIL . (INDUCTION#10) . NIL . INDUCTION . NIL . 10 .)(|¬(∃DESC.(∀N.DESC(N')<DESC(N)))| . (AXIOM (TM& . |¬(∃DESC.(∀N.DESC(N')<DESC(N)))|)) . (LESSP ADD1 M N K J I (DESC . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#11 . NIL . VARIABLE .))) . NIL . (INDUCTION#11) . NIL . INDUCTION . NIL . 11 .)(NIL . (DECL INISET (TYPE: (TY& . @SET))) . ((INISET . (@SET . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#12 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . INDUCTION . NIL . 12 .)(NIL . (DECL SETSEQ (TYPE: (TY& . |GROUND→(@SET)|))) . ((SETSEQ . (|GROUND→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#13 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . INDUCTION . NIL . 13 .)(NIL . (DECL INDSCLAUSE (TYPE: (TY& . |((@SET)⊗GROUND)→(@SET)|))) . ((INDSCLAUSE . (|((@SET)⊗GROUND)→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#14 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . INDUCTION . NIL . 14 .)(|∀INISET INDSCLAUSE.(∃SETSEQ.SETSEQ(0)=INISET∧ (∀N.SETSEQ(N')=INDSCLAUSE(SETSEQ(N),N)))| . (AXIOM (TM& . |∀INISET INDSCLAUSE.(∃SETSEQ.SETSEQ(0)=INISET∧ (∀N.SETSEQ(N')=INDSCLAUSE(SETSEQ(N),N)))|)) . (ADD1 M N K J I SET INISET SETSEQ INDSCLAUSE) . NIL . (INDUCTION#15) . NIL . INDUCTION . NIL . 15 .)(|∀N.UNIV(N)=TRUE| . (DEFINE UNIV (TM& . |∀N.UNIV(N)=TRUE|) NIL) . (M N K J I SET (UNIV . (@SET . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#4 . NIL . DEFINED .))) . NIL . (SET#4 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32) . NIL . SET . NIL . 4 .)(NIL . (DECL INTERSECTION (TYPE: (TY& . |((@SET)⊗(@SET))→(@SET)|)) (INFIXNAME: ∩) (BINDINGPOWER: 950) (PREFIXNAME: INTERSECTION)) . ((INTERSECTION . (|((@SET)⊗(@SET))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SET#5 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SET . NIL . 5 .)(|∀A B.A∩B=(λXV.A(XV)∧B(XV))| . (DEFINE INTERSECTION (TM& . |∀A B.A∩B=(λXV.A(XV)∧B(XV))|) NIL) . (SET C B A (INTERSECTION . (|((@SET)⊗(@SET))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INTERSECTION) (BINDP& . 950) (INFIX& . ∩)) . SET#6 . NIL . DEFINED .)) (XV . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#6 . NIL . VARIABLE .))) . NIL . (SET#6 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4) . NIL . SET . NIL . 6 .)(NIL . (DECL UNION (TYPE: (TY& . |((@SET)⊗(@SET))→(@SET)|)) (INFIXNAME: ∪) (BINDINGPOWER: 950) (PREFIXNAME: UNION)) . ((UNION . (|((@SET)⊗(@SET))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SET#7 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SET . NIL . 7 .)(|∀A B.A∪B=(λXV.A(XV)∨B(XV))| . (DEFINE UNION (TM& . |∀A B.A∪B=(λXV.A(XV)∨B(XV))|) NIL) . (SET C B A INTERSECTION XV (UNION . (|((@SET)⊗(@SET))→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . UNION) (BINDP& . 950) (INFIX& . ∪)) . SET#8 . NIL . DEFINED .))) . NIL . (SET#8 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4) . NIL . SET . NIL . 8 .)(NIL . (DECL INCLUSION (TYPE: (TY& . |((@SET)⊗(@SET))→TRUTHVAL|)) (INFIXNAME: ⊂) (BINDINGPOWER: 920) (PREFIXNAME: INCLUSION)) . ((INCLUSION . (|((@SET)⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SET#9 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SET . NIL . 9 .)(|∀A B.A⊂B≡(∀N.A(N)⊃B(N))| . (DEFINE INCLUSION (TM& . |∀A B.A⊂B≡(∀N.A(N)⊃B(N))|) NIL) . (M N K J I SET C B A (INCLUSION . (|((@SET)⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((PREFIX& . INCLUSION) (BINDP& . 920) (INFIX& . ⊂)) . SET#10 . NIL . DEFINED .))) . NIL . (SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4) . NIL . SET . NIL . 10 .)(NIL . (DECL INVERSE (TYPE: (TY& . |((@FUNCT)⊗(@SET)⊗GROUND)→(@SET)|))) . ((INVERSE . (|((@FUNCT)⊗(@SET)⊗GROUND)→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#11 . NIL . VARIABLE .)) SET FUNCT) . NIL . NIL . NIL . SET . NIL . 11 .)(|∀F A N.INVERSE(F,A,N)=(λXV.A(XV)∧F(XV)=N)| . (DEFINE INVERSE (TM& . |∀F A N.INVERSE(F,A,N)=(λXV.A(XV)∧F(XV)=N)|) NIL) . (M N K J I SET C B A FUNCT F INTERSECTION XV (INVERSE . (|((@FUNCT)⊗(@SET)⊗GROUND)→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#12 . NIL . DEFINED .))) . NIL . (SET#12 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4) . NIL . SET . NIL . 12 .)(|∀F A N.INVERSE(F,A,N)⊂A| . (TRW (TM& . |∀F A N.INVERSE(F,A,N)⊂A|) (OPEN INVERSE INCLUSION)) . (M N K J I SET C B A FUNCT F INTERSECTION XV INCLUSION INVERSE) . NIL . (SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4) . NIL . SET . NIL . 13 .)(|∀F A.(∀N.F(N)=0∨F(N)=1)⊃A⊂INVERSE(F,A,0)∪INVERSE(F,A,1)| . (TRW (TM& . |∀F A.(∀N.F(N)=0∨F(N)=1)⊃A⊂INVERSE(F,A,0)∪INVERSE(F,A,1)|) (OPEN INVERSE INCLUSION UNION)) . (M N K J I SET C B A FUNCT F INTERSECTION XV UNION INCLUSION INVERSE) . NIL . (SET#12 SET#10 SET#8 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13) . NIL . SET . NIL . 14 .)(NIL . (DECL EPSILON (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (INFIXNAME: ε) (BINDINGPOWER: 925)) . ((EPSILON . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SET#15 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SET . NIL . 15 .)(|∀A N.NεA≡A(N)| . (DEFINE EPSILON (TM& . |∀A N.NεA≡A(N)|) NIL) . (M N K J I SET C B A (EPSILON . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SET#16 . NIL . DEFINED .))) . NIL . (SET#16 SET#8 SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14) . NIL . SET . NIL . 16 .)(NIL . (DECL TRANSITIVE (TYPE: (TY& . |(@REL)→TRUTHVAL|))) . ((TRANSITIVE . (|(@REL)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#17 . NIL . VARIABLE .)) REL) . NIL . NIL . NIL . SET . NIL . 17 .)(|∀REL.TRANSITIVE(REL)≡(∀N M K.REL(N,M)∧REL(M,K)⊃REL(N,K))| . (DEFINE TRANSITIVE (TM& . |∀REL.TRANSITIVE(REL)≡(∀N M K.REL(N,M)∧REL(M,K)⊃REL(N,K))|) NIL) . (M N K J I REL (TRANSITIVE . (|(@REL)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#18 . NIL . DEFINED .))) . NIL . (SET#18 SET#8 SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14) . NIL . SET . NIL . 18 .)(NIL . (DECL SEGM (TYPE: (TY& . |GROUND→(@SET)|))) . ((SEGM . (|GROUND→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#19 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SET . NIL . 19 .)(|∀N.SEGM(N)=(λXV.XV<N)| . (DEFINE SEGM (TM& . |∀N.SEGM(N)=(λXV.XV<N)|) NIL) . (LESSP M N K J I SET C B A INTERSECTION XV (SEGM . (|GROUND→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#20 . NIL . DEFINED .))) . NIL . (SET#20 SET#8 SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14) . NIL . SET . NIL . 20 .)(NIL . (DECL TAIL (TYPE: (TY& . |GROUND→(@SET)|))) . ((TAIL . (|GROUND→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#21 . NIL . VARIABLE .)) SET) . NIL . NIL . NIL . SET . NIL . 21 .)(|∀N.TAIL(N)=(λXV.N<XV)| . (DEFINE TAIL (TM& . |∀N.TAIL(N)=(λXV.N<XV)|) NIL) . (LESSP M N K J I SET C B A INTERSECTION XV (TAIL . (|GROUND→(@SET)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SET#22 . NIL . DEFINED .))) . NIL . (SET#22 SET#8 SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14) . NIL . SET . NIL . 22 .)(|∀A.(∃N.A(N))≡A(MIN(A))| . (TRW (TM& . |∀A.(∃N.A(N))≡A(MIN(A))|) (DER (LR& MINMAX#9))) . (M N K J I SET C B A MIN) . NIL . (SET#8 SET#12 SET#10 MINMAX#9 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8) . NIL . MINMAX . NIL . 11 .)(|∀REL.TRANSITIVE(REL)∧(∀N.REL(N,N'))⊃(∀N M.N<M⊃REL(N,M))| . (AXIOM (TM& . |∀REL.TRANSITIVE(REL)∧(∀N.REL(N,N'))⊃(∀N M.N<M⊃REL(N,M))|)) . (LESSP ADD1 M N K J I REL TRANSITIVE) . NIL . (INDUCTION#16) . NIL . INDUCTION . NIL . 16 .)(|∀INDCCLAUSE.(∃A.(∀N.A(N)≡INDCCLAUSE(A∩SEGM(N),N)))| . (AXIOM (TM& . |∀INDCCLAUSE.(∃A.(∀N.A(N)≡INDCCLAUSE(A∩SEGM(N),N)))|)) . (LESSP M N K J I SET C B A INTERSECTION XV SEGM (INDCCLAUSE . (|((GROUND→TRUTHVAL)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#17 . NIL . VARIABLE .))) . NIL . (INDUCTION#17) . NIL . INDUCTION . NIL . 17 .)(|∀A.UNBOUND(A)≡¬(∃N.A⊂SEGM(N))| . (DEFINE UNBOUND (TM& . |∀A.UNBOUND(A)≡¬(∃N.A⊂SEGM(N))|) NIL) . (LESSP M N K J I SET C B A INTERSECTION XV INCLUSION SEGM (UNBOUND . (|(@SET)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . UNBOUND#2 . NIL . DEFINED .))) . NIL . (UNBOUND#2 SET#8 SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8) . NIL . UNBOUND . NIL . 2 .)(|UNBOUND(UNIV)| . (TRW (TM& . |UNBOUND(UNIV)|) ((OPEN UNBOUND INCLUSION SEGM) (DER (LR& NATNUM#7)))) . (LESSP M N K J I SET C B A UNIV INTERSECTION XV INCLUSION SEGM UNBOUND) . NIL . (SET#20 SET#8 SET#12 SET#10 NATNUM#7 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8 UNBOUND#2) . NIL . UNBOUND . NIL . 3 .)(|∀A B C.A⊂B∪C∧UNBOUND(A)⊃UNBOUND(B)∨UNBOUND(C)| . (TRW (TM& . |∀A B C.A⊂B∪C∧UNBOUND(A)⊃UNBOUND(B)∨UNBOUND(C)|) ((OPEN UNBOUND INCLUSION SEGM UNION) (DER (LR& MINMAX#5)))) . (LESSP M N K J I SET C B A INTERSECTION XV UNION INCLUSION SEGM UNBOUND) . NIL . (NATNUM#7 SET#20 SET#12 SET#10 SET#8 MINMAX#5 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8 UNBOUND#2 UNBOUND#3) . NIL . UNBOUND . NIL . 4 .)(|∀A.BOUND(A)=MIN(λXV.A⊂SEGM(XV))| . (DEFINE BOUND (TM& . |∀A.BOUND(A)=MIN(λXV.A⊂SEGM(XV))|) NIL) . (LESSP M N K J I SET C B A INTERSECTION XV INCLUSION SEGM MIN (BOUND . (|(GROUND→TRUTHVAL)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . UNBOUND#5 . NIL . DEFINED .))) . NIL . (UNBOUND#5 SET#20 NATNUM#7 SET#8 SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8 UNBOUND#2 UNBOUND#3) . NIL . UNBOUND . NIL . 5 .)(|∀A.NATNUM(BOUND(A))| . (TRW (TM& . |∀A.NATNUM(BOUND(A))|) (OPEN BOUND)) . (LESSP M N K J I SET C B A INTERSECTION XV INCLUSION SEGM MIN BOUND) . NIL . (UNBOUND#5 SET#20 NATNUM#7 SET#8 SET#12 SET#10 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8 UNBOUND#2 UNBOUND#3) . NIL . UNBOUND . NIL . 6 .)(|∀A.¬UNBOUND(A)≡A⊂SEGM(BOUND(A))| . (TRW (TM& . |∀A.¬UNBOUND(A)≡A⊂SEGM(BOUND(A))|) ((OPEN BOUND UNBOUND) (USE (LR& MINMAX#11) MODE: EXACT UE: (UELST& (A . |λXV.A⊂SEGM(XV)|))))) . (LESSP M N K J I SET C B A INTERSECTION XV INCLUSION SEGM MIN UNBOUND BOUND) . NIL . (UNBOUND#5 SET#20 NATNUM#7 SET#8 SET#12 SET#10 MINMAX#9 NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32 SET#4 SET#13 SET#14 MINMAX#3 MINMAX#4 MINMAX#7 MINMAX#8 UNBOUND#2 UNBOUND#3 UNBOUND#6) . NIL . UNBOUND . NIL . 7 .)